Nuprl Lemma : locknd-deq_wf
11,40
postcript
pdf
locknd-deq()
EqDecider(LocKnd)
latex
Definitions
Knd
,
t
T
,
Id
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
strong-subtype(
A
;
B
)
,
hasloc(
k
;
i
)
,
b
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
Type
,
,
x
.
A
(
x
)
,
P
Q
,
x
.
t
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
EqDecider(
T
)
,
KindDeq
,
IdDeq
,
product-deq(
A
;
B
;
a
;
b
)
,
locknd-deq()
,
LocKnd
Lemmas
product-deq
wf
,
id-deq
wf
,
Kind-deq
wf
,
strong-subtype-deq-subtype
,
strong-subtype-set3
,
assert
wf
,
hasloc
wf
,
strong-subtype-self
,
Id
wf
,
Knd
wf
origin
T, Id, x:A 
B(x), 
x:A. B(x), strong-subtype(A;B), hasloc(k;i), 
b, let x,y = A in B(x;y), Type, 
, 
x.A(x), P 
Q, 
x. t(x), {x:A| B(x)} , EqDecider(T), KindDeq, IdDeq, product-deq(A;B;a;b), locknd-deq(), LocKnd